Issue478c.agda:9,12-15
Set₁ !=< Ko.T ko
when checking that the expression Set has type Ko.T ko
